{-# OPTIONS -fglasgow-exts #-}

-----------------------------------------------------------------------------
-- |
-- Maintainer  :  2LT Team
--
-- Support for data type constraints (invariants)
--
-----------------------------------------------------------------------------

module Data.Transform.Constraints where

import Data.Transform.Rule
import Data.Transform.RulesPF (simplifyPF)
import Control.Monad

-----------------------------------------------------------------------------
-- * Some basic rules

-- | Logical composition of nested constraints
compose_constraint :: Rule
compose_constraint (TInv (TInv a phi) psi)
   = return $ View idrep (TInv a (AND phi psi))
compose_constraint _ = mzero

-- | Simplify constraint by point-free program calculation
fuse_constraint :: Rule
fuse_constraint (TInv a phi) = do
  psi <- simplifyPF (Func a Bool) phi
  return $View idrep (TInv a psi)
fuse_constraint _ = mzero

-- | Propagate existing constraint on the input type through
--   the application of a rule to the output type.
propagate :: (Type a -> Maybe (View (Type a))) 
          -> Type a -> Maybe (View (Type a))
propagate r (TInv t inv) = do
   (View rep tb) <- r t
   let inv' = COMP t inv (from rep)
   return $ View rep (TInv tb inv')
propagate _ _ = mzero

-----------------------------------------------------------------------------
